0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 83 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 3 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 MRRProof (⇔, 12 ms)
↳22 QDP
↳23 PisEmptyProof (⇔, 0 ms)
↳24 YES
logB_in_ga(0, s(0)) → logB_out_ga(0, s(0))
logB_in_ga(s(0), s(s(0))) → logB_out_ga(s(0), s(s(0)))
logB_in_ga(s(s(T10)), s(T7)) → U2_ga(T10, T7, halfA_in_ga(T10, X18))
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T14)), s(X27)) → U1_ga(T14, X27, halfA_in_ga(T14, X27))
U1_ga(T14, X27, halfA_out_ga(T14, X27)) → halfA_out_ga(s(s(T14)), s(X27))
U2_ga(T10, T7, halfA_out_ga(T10, X18)) → logB_out_ga(s(s(T10)), s(T7))
logB_in_ga(s(s(T10)), s(T7)) → U3_ga(T10, T7, halfA_in_ga(T10, T11))
U3_ga(T10, T7, halfA_out_ga(T10, T11)) → U4_ga(T10, T7, logB_in_ga(s(T11), T7))
U4_ga(T10, T7, logB_out_ga(s(T11), T7)) → logB_out_ga(s(s(T10)), s(T7))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
logB_in_ga(0, s(0)) → logB_out_ga(0, s(0))
logB_in_ga(s(0), s(s(0))) → logB_out_ga(s(0), s(s(0)))
logB_in_ga(s(s(T10)), s(T7)) → U2_ga(T10, T7, halfA_in_ga(T10, X18))
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T14)), s(X27)) → U1_ga(T14, X27, halfA_in_ga(T14, X27))
U1_ga(T14, X27, halfA_out_ga(T14, X27)) → halfA_out_ga(s(s(T14)), s(X27))
U2_ga(T10, T7, halfA_out_ga(T10, X18)) → logB_out_ga(s(s(T10)), s(T7))
logB_in_ga(s(s(T10)), s(T7)) → U3_ga(T10, T7, halfA_in_ga(T10, T11))
U3_ga(T10, T7, halfA_out_ga(T10, T11)) → U4_ga(T10, T7, logB_in_ga(s(T11), T7))
U4_ga(T10, T7, logB_out_ga(s(T11), T7)) → logB_out_ga(s(s(T10)), s(T7))
LOGB_IN_GA(s(s(T10)), s(T7)) → U2_GA(T10, T7, halfA_in_ga(T10, X18))
LOGB_IN_GA(s(s(T10)), s(T7)) → HALFA_IN_GA(T10, X18)
HALFA_IN_GA(s(s(T14)), s(X27)) → U1_GA(T14, X27, halfA_in_ga(T14, X27))
HALFA_IN_GA(s(s(T14)), s(X27)) → HALFA_IN_GA(T14, X27)
LOGB_IN_GA(s(s(T10)), s(T7)) → U3_GA(T10, T7, halfA_in_ga(T10, T11))
U3_GA(T10, T7, halfA_out_ga(T10, T11)) → U4_GA(T10, T7, logB_in_ga(s(T11), T7))
U3_GA(T10, T7, halfA_out_ga(T10, T11)) → LOGB_IN_GA(s(T11), T7)
logB_in_ga(0, s(0)) → logB_out_ga(0, s(0))
logB_in_ga(s(0), s(s(0))) → logB_out_ga(s(0), s(s(0)))
logB_in_ga(s(s(T10)), s(T7)) → U2_ga(T10, T7, halfA_in_ga(T10, X18))
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T14)), s(X27)) → U1_ga(T14, X27, halfA_in_ga(T14, X27))
U1_ga(T14, X27, halfA_out_ga(T14, X27)) → halfA_out_ga(s(s(T14)), s(X27))
U2_ga(T10, T7, halfA_out_ga(T10, X18)) → logB_out_ga(s(s(T10)), s(T7))
logB_in_ga(s(s(T10)), s(T7)) → U3_ga(T10, T7, halfA_in_ga(T10, T11))
U3_ga(T10, T7, halfA_out_ga(T10, T11)) → U4_ga(T10, T7, logB_in_ga(s(T11), T7))
U4_ga(T10, T7, logB_out_ga(s(T11), T7)) → logB_out_ga(s(s(T10)), s(T7))
LOGB_IN_GA(s(s(T10)), s(T7)) → U2_GA(T10, T7, halfA_in_ga(T10, X18))
LOGB_IN_GA(s(s(T10)), s(T7)) → HALFA_IN_GA(T10, X18)
HALFA_IN_GA(s(s(T14)), s(X27)) → U1_GA(T14, X27, halfA_in_ga(T14, X27))
HALFA_IN_GA(s(s(T14)), s(X27)) → HALFA_IN_GA(T14, X27)
LOGB_IN_GA(s(s(T10)), s(T7)) → U3_GA(T10, T7, halfA_in_ga(T10, T11))
U3_GA(T10, T7, halfA_out_ga(T10, T11)) → U4_GA(T10, T7, logB_in_ga(s(T11), T7))
U3_GA(T10, T7, halfA_out_ga(T10, T11)) → LOGB_IN_GA(s(T11), T7)
logB_in_ga(0, s(0)) → logB_out_ga(0, s(0))
logB_in_ga(s(0), s(s(0))) → logB_out_ga(s(0), s(s(0)))
logB_in_ga(s(s(T10)), s(T7)) → U2_ga(T10, T7, halfA_in_ga(T10, X18))
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T14)), s(X27)) → U1_ga(T14, X27, halfA_in_ga(T14, X27))
U1_ga(T14, X27, halfA_out_ga(T14, X27)) → halfA_out_ga(s(s(T14)), s(X27))
U2_ga(T10, T7, halfA_out_ga(T10, X18)) → logB_out_ga(s(s(T10)), s(T7))
logB_in_ga(s(s(T10)), s(T7)) → U3_ga(T10, T7, halfA_in_ga(T10, T11))
U3_ga(T10, T7, halfA_out_ga(T10, T11)) → U4_ga(T10, T7, logB_in_ga(s(T11), T7))
U4_ga(T10, T7, logB_out_ga(s(T11), T7)) → logB_out_ga(s(s(T10)), s(T7))
HALFA_IN_GA(s(s(T14)), s(X27)) → HALFA_IN_GA(T14, X27)
logB_in_ga(0, s(0)) → logB_out_ga(0, s(0))
logB_in_ga(s(0), s(s(0))) → logB_out_ga(s(0), s(s(0)))
logB_in_ga(s(s(T10)), s(T7)) → U2_ga(T10, T7, halfA_in_ga(T10, X18))
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T14)), s(X27)) → U1_ga(T14, X27, halfA_in_ga(T14, X27))
U1_ga(T14, X27, halfA_out_ga(T14, X27)) → halfA_out_ga(s(s(T14)), s(X27))
U2_ga(T10, T7, halfA_out_ga(T10, X18)) → logB_out_ga(s(s(T10)), s(T7))
logB_in_ga(s(s(T10)), s(T7)) → U3_ga(T10, T7, halfA_in_ga(T10, T11))
U3_ga(T10, T7, halfA_out_ga(T10, T11)) → U4_ga(T10, T7, logB_in_ga(s(T11), T7))
U4_ga(T10, T7, logB_out_ga(s(T11), T7)) → logB_out_ga(s(s(T10)), s(T7))
HALFA_IN_GA(s(s(T14)), s(X27)) → HALFA_IN_GA(T14, X27)
HALFA_IN_GA(s(s(T14))) → HALFA_IN_GA(T14)
From the DPs we obtained the following set of size-change graphs:
LOGB_IN_GA(s(s(T10)), s(T7)) → U3_GA(T10, T7, halfA_in_ga(T10, T11))
U3_GA(T10, T7, halfA_out_ga(T10, T11)) → LOGB_IN_GA(s(T11), T7)
logB_in_ga(0, s(0)) → logB_out_ga(0, s(0))
logB_in_ga(s(0), s(s(0))) → logB_out_ga(s(0), s(s(0)))
logB_in_ga(s(s(T10)), s(T7)) → U2_ga(T10, T7, halfA_in_ga(T10, X18))
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T14)), s(X27)) → U1_ga(T14, X27, halfA_in_ga(T14, X27))
U1_ga(T14, X27, halfA_out_ga(T14, X27)) → halfA_out_ga(s(s(T14)), s(X27))
U2_ga(T10, T7, halfA_out_ga(T10, X18)) → logB_out_ga(s(s(T10)), s(T7))
logB_in_ga(s(s(T10)), s(T7)) → U3_ga(T10, T7, halfA_in_ga(T10, T11))
U3_ga(T10, T7, halfA_out_ga(T10, T11)) → U4_ga(T10, T7, logB_in_ga(s(T11), T7))
U4_ga(T10, T7, logB_out_ga(s(T11), T7)) → logB_out_ga(s(s(T10)), s(T7))
LOGB_IN_GA(s(s(T10)), s(T7)) → U3_GA(T10, T7, halfA_in_ga(T10, T11))
U3_GA(T10, T7, halfA_out_ga(T10, T11)) → LOGB_IN_GA(s(T11), T7)
halfA_in_ga(0, 0) → halfA_out_ga(0, 0)
halfA_in_ga(s(0), 0) → halfA_out_ga(s(0), 0)
halfA_in_ga(s(s(T14)), s(X27)) → U1_ga(T14, X27, halfA_in_ga(T14, X27))
U1_ga(T14, X27, halfA_out_ga(T14, X27)) → halfA_out_ga(s(s(T14)), s(X27))
LOGB_IN_GA(s(s(T10))) → U3_GA(halfA_in_ga(T10))
U3_GA(halfA_out_ga(T11)) → LOGB_IN_GA(s(T11))
halfA_in_ga(0) → halfA_out_ga(0)
halfA_in_ga(s(0)) → halfA_out_ga(0)
halfA_in_ga(s(s(T14))) → U1_ga(halfA_in_ga(T14))
U1_ga(halfA_out_ga(X27)) → halfA_out_ga(s(X27))
halfA_in_ga(x0)
U1_ga(x0)
LOGB_IN_GA(s(s(T10))) → U3_GA(halfA_in_ga(T10))
U3_GA(halfA_out_ga(T11)) → LOGB_IN_GA(s(T11))
halfA_in_ga(0) → halfA_out_ga(0)
halfA_in_ga(s(0)) → halfA_out_ga(0)
halfA_in_ga(s(s(T14))) → U1_ga(halfA_in_ga(T14))
U1_ga(halfA_out_ga(X27)) → halfA_out_ga(s(X27))
U3GA1 > LOGBINGA1 > s1 > halfAinga1 > halfAoutga1 > 0 > U1ga1
0=1
halfA_in_ga_1=7
halfA_out_ga_1=6
s_1=4
U1_ga_1=5
LOGB_IN_GA_1=5
U3_GA_1=3
halfA_in_ga(x0)
U1_ga(x0)